es:ES, ff:FIFO, p:(E), e:E, sndr, rcvr:ff.C.
(ff.C r Id)
 (i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i  Id))
 [e: sndr p rcvr]
 (loc(e) = sndr  Id) 

latex

Definitions	t  T, P  Q, , x:A. B(x), P & Q, [e: i p j]
Lemmas	event system wf, FIFO wf, es-loc wf, Id wf, fifoR wf, es-E wf, fifoC wf, rcv-it wf